Lean is a functional programming language that is designed to be used for theorem proving. Functions in lean which compile can be directly mapped to theorems, making the lean compiler a powerful tool for theorem verification. I will describe the basics of of lean, and build up towards the definitions and structures needed in quantum information. The particular theorem we will work towards is the security guarantee of the bb84 quantum key distribution protocol. The seminar is intended to be accessible for physicists with no prior knowledge of lean.

BSc: Victoria university of Wellington, New Zealand. MSc+PhD: Uppsala University, Sweden Postdoc: Humboldt University, Berlin, Germany Postdoc: MIT